Nuprl Definition : es-seq 0,22

es-seq(es;S) == e1e2:E. e1 before e2  S  (e2 < e1
latex



clarification:

es-seq(es;S)
== e1:es-E(es), e2:es-E(es). e1 before e2  S  es-E(es es-causl(ese2e1
latex


Definitionsx:AB(x), P  Q, x before y  l, E, A, (e < e')
FDL editor aliaseses-seq

origin